\ifx\wholebook\relax \else

\documentclass[UTF8]{article}

\usepackage[cn]{../../prelude}

\setcounter{page}{1}

\begin{document}

\title{自然数}

\author{刘新宇
\thanks{{\bfseries 刘新宇} \newline
  Email: liuxinyu95@gmail.com \newline}
  }

\maketitle
\fi

\markboth{自然数}{编程中的数学}

\chapter*{加法交换律的证明}
\phantomsection  % so hyperref creates bookmarks
\addcontentsline{toc}{chapter}{加法交换律的证明}

为了证明加法交换律$a + b = b + a$。我们首先证明三个结论。第一个是说对于任何自然数都有：

\be
0 + a = a
\label{eq:left-zero}
\ee

也就是说，加法左侧的零可以消去。首先看起始情况，当$a=0$时，根据加法定义的第一条规则有：

\[
0 + 0 = 0
\]

其次是递推情况，设$0 + a = a$，我们要推出$0 + a' = a'$。

\[
\begin{array}{rlr}
0 + a' & = (0 + a)' & \text{加法定义的规则二} \\
       & = a' & \text{递推假设}
\end{array}
\]

接下来我们定义0的后继为1，并证明第二个重要结论：

\be
a' = a + 1
\label{eq:one-succ}
\ee

也就是说，任何自然的后继，等于这个自然数加一。这是因为：

\[
\begin{array}{rlr}
a' & = (a + 0)' & \text{加法定义的规则一} \\
   & = a + 0' & \text{加法定义的规则二} \\
   & = a + 1 & \text{定义0的后继是1}
\end{array}
\]

第三个要证明的结论是交换律的一个特例：

\be
a + 1 = 1 + a
\label{eq:one-commu}
\ee

首先看$a = 0$的起始情况。

\[
\begin{array}{rlr}
0 + 1 & = 1 & \text{刚证明的加法左侧零可消去} \\
      & = 1 + 0 & \text{加法定义的第一条规则}
\end{array}
\]

然后是递推情况，设$a + 1 = 1 + a$成立，我们要推出$a' + 1 = 1 + a'$。

\[
\begin{array}{rlr}
a' + 1 & = a' + 0' & \text{1是0的后继} \\
       & = (a' + 0)' & \text{加法定义的第一条规则} \\
       & = ((a + 1) + 0)' & \text{根据刚刚证明的结论二} \\
       & = (a + 1)' & \text{加法定义的规则一} \\
       & = (1 + a)' & \text{递推假设} \\
       & = 1 + a' & \text{加法定义的规则二}
\end{array}
\]

有了这三个结论，我们就可以着手证明加法交换律了。我们首先证明$b=0$时交换律成立。根据加法定义的规则一，我们有$a + 0 = a$；同时根据刚才证明的结论一，又有$0 + a = a$。这就证明了$a + 0 = 0 + a$。
然后我们证明递推情况。假设$a + b = b + a$成立，我们要推出$a + b' = b' + a$。

\[
\begin{array}{rlr}
a + b' & = (a + b)' & \text{根据加法定义的第二条规则} \\
       & = (b + a)' & \text{递推假设} \\
       & = b + a' & \text{加法定义的第二条规则} \\
       & = b + a + 1 & \text{刚刚证明的结论二，即(\ref{eq:one-succ})} \\
       & = b + 1 + a & \text{刚刚证明的结论三，即(\ref{eq:one-commu})} \\
       & = (b + 1) + a & \text{第一章证明的加法结合律} \\
       & = b' + a & \text{刚刚证明的结论三，即(\ref{eq:one-commu})}
\end{array}
\]

这样我们就使用皮亚诺公理，完整地证明了加法的交换律(\cite{StepanovRose15}, p147-148)。

\ifx\wholebook\relax \else
\begin{thebibliography}{99}

\bibitem{StepanovRose15}
[美] 亚历山大 A$\cdot$斯捷潘诺夫，丹尼尔 E$\cdot$罗斯著，爱飞翔译. ``数学与泛型编程：高效编程的奥秘''. 机械工业出版社. 2017, ISBN: 9787111576587
\end{thebibliography}

\expandafter\enddocument
%\end{document}

\fi
